Dafny: Implement and Verify Modular Programs

Dafny is a verification-aware programming language that integrates specification and verification into the programming process. In this lab project, students will choose a small but non-trivial program they are interested in and implement it in Dafny, including formal specifications and correctness proofs. Programs should be modular, with clearly defined functions and correctness conditions (e.g., functional correctness, termination).

Students are encouraged to propose their own project ideas. Two examples to start from:

• A priority queue with formally verified enqueue/dequeue behavior.
• A basic interpreter for arithmetic expressions with verified evaluation semantics.

The scope can be scaled during the semester depending on progress and complexity.

Starting Points

• \link{https://github.com/dafny-lang/dafny}
• \link{https://dafny.org/dafny/}
• \link{https://dafny.org/dafny/toc}
• \link{Dafny: An Automatic Program Verifier for Functional Correctness; https://www.microsoft.com/en-us/research/wp-content/uploads/2008/12/dafny_krml203.pdf}